Inference at * 1 1 
Iof proof for Lemma comp nat ind a:

.....assertion..... NILNIL

1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. 
  j,s:. (s < j)  P(s) 

latex

 by (% do simple nat induction% 
((((BLemma `nat_ind_a`) 
(CollapseTHENM (RepD))) 

(CoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
(C) inil_term)))) 

latex

(C1: 

(C1: 4. s : 
(C1: 5. s < 0
(C1:   P(s)
(C2: 

(C2: 4. j : 
(C2: 5. s:. (s < (j - 1))  P(s)
(C2: 6. s : 
(C2: 7. s < j
(C2:   P(s)
(C.

Definitions	t  T, x. t(x), x(s), P  Q, x:A. B(x), , {T}, ,
Lemmas	nat plus wf, nat wf, nat ind a